1. Field of the Invention
The present invention relates to a computer implemented method for verifying that a circuit or other system satisfies its specification, which operates at a low level and is based on quantified Boolean logic rather than first-order or higher-order logic.
2. Background of the Prior Art
Errors in the design of complex systems, such as computer chips, can be very costly. Computer chip verification (also referred to herein as computer hardware verification) determines whether the circuitry on a computer chip or other computer hardware device operates properly, typically in accordance with its specifications. Since computer chip verification is one of the most expensive facets of chip design, there is substantial interest in the industry aimed at finding cheaper and faster verification methods.
The general method known in the art, by which Boolean formulae are used, by computer programs for system testing is the following:
(1) A Boolean formula G is constructed from a system S and its specification, expressing that the system does not satisfy its specification. Methods for generating G are well known. PA1 (2) The formula G is tested for satisfiability (consistency). PA1 (3) If G is unsatisfiable, then S is correct. If G is satisfiable, then there is an error in S, and the nature of the satisfiability of G can help to identify the error in S.
G can also be constructed to express that S does satisfy its specification and then G is tested to determine if it is a tautology, if so, S is correct, if not S is incorrect.
The system S can be a computer circuit or some system containing interconnected objects, which can be defined as a component or part of a physical system, such as a gate in a circuit. A general explanation for the method known in the art by which Boolean formulae are used for system testing is to define A as a Boolean formula representing the system S and B is a Boolean formula representing the statement that S fails to satisfy its specification. Then G can be taken to be the conjunction AB of these two formulae, expressing that S fails to satisfy its specification. If AB is unsatisfiable, this means that there is no way that S can fail to satisfy its specification, so S satisfies its specification. If AB is satisfiable, there is an error in S. There are also other ways in which G can be generated from A and B. These other ways include the disjunction ((not A) or (not B)) which expresses that S does satisfy its specification.
Discussed briefly below are known examples of different methods used to verify the correctness of any system of interconnected objects.
As stated above, it is generally known in the art that a circuit can be verified by translating the circuit into Boolean formulae and testing the formulae for satisfiability. Typical satisfiability tests process the whole formula at once. One method of representing a circuit by a Boolean formula for testing purposes is given in (Larrabee, Tracy, Test Pattern Generation using Boolean Satisfiability, IEEE Transactions on Computer-Aided Design 11:1 (January, 1992) 4-15). Larrabee conducts the satisfiability tests in a way that involves looking for a pattern of inputs that will cause certain kinds of errors to appear.
Recently, binary decision diagrams (BDD's) have become very popular with chip designers because they permit the verification of the equivalence of two circuits with computer assistance without explicit testing on all inputs. BDD's transform a circuit into a canonical form, depending on an ordering of the Boolean variables, and two circuits are equivalent if and only if they have the same canonical form. For many kinds of circuits, BDD's work very well, especially when a good ordering of the variables can be found. Testing equivalence is important, because one can verify a new or optimized circuit by showing that it is equivalent to an old and trusted circuit. BDD's are presented in Bryant, R. E., Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers 35:8 (1986) 677-691.
Another approach to hardware verification is to use an expressive theorem prover such as high-order logic (HOL) for this purpose. This approach is described in the paper (A. Camilleri, M. Gordon, and T. Melham, "Hardware Verification using Higher-Order Logic," Proceedings of the International Federation for Information Processing International Working Conference: From HDL Descriptions to Guaranteed Correct Circuit Designs, Grenoble, France, Sep. 9-11, 1986). Another expressive verifier for formal design validation is described in (N. Shankar, S. Owre, and J. M. Rushby, "The PVS Proof Checker: A reference manual," Computer Science Laboratory, SRI International, Menlo Park, Calif., 1993). The use of such high-level provers permits proofs of complex systems to be achieved. The disadvantage of using HOL or a high-level language is that such HOL or high-level proofs are time consuming and may not verify the correctness of a hardware circuit at the gate level.
Another method of verifying the correctness of a hardware circuit is by specifying the system's design using a high-level language such as VHDL (IEEE Standard VHDL Language Reference Manual (IEEE Std 1076-1987)), and then transforming this design to the register level (specifying how the contents of one register at a given time depend on the contents of other registers at the preceding time). Verification with a high-level language involves testing the circuit and determining whether it operates in accordance with a VHDL specification. However, the VHDL analysis does not specify how the circuit is implemented by gates. To determine how a circuit is implemented by gates, the VHDL specification would need to be transformed into a register level and then to the gate level, and verified again. The system at the gate level can be represented, of course, by Boolean formulae. Finally, once the chip's design is determined to be correct, the design is transformed to the silicon level.
Satisfiability algorithms for Boolean formulae in clause form can also be used for hardware verification. In this approach, the circuit is transformed into a formula in clause form, which is a special form of unquantified Boolean formula. The specification of the circuit is also translated into a formula, and these two formulae are combined to obtain a formula expressing that the circuit is correct (or incorrect). An efficient method such as Davis and Putnam's method can then be applied to test if the formula is satisfiable. This method was first described in the paper (Davis, M. and Putnam, H., A computing procedure for quantification theory, J. ACM 7 (1960) 201-215), though modern implementations differ in some ways. If the Boolean formula expresses that the circuit is incorrect, and the Boolean formula is unsatisfiable, then the circuit is correct. If the formula is satisfiable, then the circuit is incorrect. If the formula expresses correctness of the circuit, then the circuit is correct if and only if the formula is a tautology, meaning, as used here, that the formula is always true. A recent, very efficient implementation of Davis and Putnam's method is described in (Zhang, H., SATO: An Efficient Propositional Prover, International Conference on Automated Deduction (CADE 97), Number 1249 in LNAI, pages 272-275, Springer-Verlag, 1997). Another method for satisfiability testing of unquantified Boolean formulae, not necessarily in clause form, is disclosed in the European Patent No. 0403 454, 1995 of Stalmarck, G., entitled A System For Determining Propositional Logic Theorems By Applying Values And Rules To Triplets That Are Generated From A Formula.
As further background, it is to be noted that symbolic model checking is concerned with verifying that systems which operate in real time are correct. Symbolic model checking is a general term that has arisen in the industry and refers to currently popular methods of verifying the correctness of any system of interconnected objects that have discrete states and interact in real time. A book about symbolic model checking is (McMillan, K. L., Symbolic Model Checking: An Approach to the State Explosion Problem (Kluwer, 1993)). The use of BDD's for symbolic model checking was a breakthrough, because it permitted much larger systems to be verified than was possible before. BDD's permit the state of a system to be represented and manipulated efficiently, in many cases. However, the paper (Biere, A., Cimatti, A., Clarke, E., and Zhu, Y., Symbolic Model Checking without BDD's, in TACAS'99, Lecture Notes in Computer Science, Springer-Verlag, 1999) gives some Boolean formulae obtained from symbolic model checking problems on which satisfiability algorithms such as Davis and Putnam's method and Stalmarck's method are more efficient than BDD's. There is therefore also an interest in seeing how far satisfiability-based approaches can extend in symbolic model checking applications.
Thus, it has been shown that satisfiability algorithms are often slower than binary decision diagrams for hardware verification. However, on certain kinds of Boolean formulae, representing systems being verified, satisfiability algorithms are faster. Thus, this invention seeks to provide a more efficient approach based on satisfiability tests that is practical for a wider variety of systems.
The Boolean formulae used for hardware verification are typically quantifier-free. However, the free variables can be regarded as universally or existentially quantified, and thus, these formulae can be regarded as quantified Boolean formulae. There are also certain additional formulae arising in symbolic model checking which are quantified. Testing equivalence of circuits can be done using quantified Boolean formulae. Thus, the present invention recognizes that quantified Boolean formulae have applications to verification methods.
With the foregoing in mind, it is the general object of the present invention to provide a method of verifying whether a system satisfies predetermined constraints, often contained in the system's specification.
It is still another object of the present invention to use satisfiability algorithms with quantified Boolean formulae by breaking down the verification process into smaller steps that are easier to perform.
It is yet another object of the present invention to find another formula F' equivalent to a formula F and providing desired subformulae.
It is also an object of the present invention to simplify F' to a formula F" having selected variables and quantifiers contained in F' removed, and to test the satisfiability of F".
The foregoing and other objects will become apparent as the description proceeds.